a, b:. ((a * b) = 0  )  ((a = 0  )  (b = 0  )) 

latex

Definitions	(i = j), tt, if b then t else f fi , qeq(r;s), b, True, T, r * s, {T}, , t  T, P  Q, P  Q, P & Q, P  Q, P  Q, x:A. B(x), False, ff, Dec(P), S  T
Lemmas	qmul comm qrng, qmul ac 1 qrng, qmul assoc qrng, qmul zero qrng, qeq wf2, assert wf, not functionality wrt iff, qinv wf, assert-qeq, qmul inv, true wf, squash wf, decidable equal rationals, int inc rationals, qmul wf, rationals wf